E,X1,X2:Type, dE:EqDecider(E), dL:EqDecider(IdLnk), pred?:(E(?E)),
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:(e:E, l:IdLnk.
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:(e':E
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:((e'':E. 
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:((rcv?(e''))
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:( (sender(e'') = e)
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:( (link(e'') = l)
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:( (((e'' = e')  e'' < e')
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:(  (loc(e') = destination(l)  Id)))),
e:E, l:IdLnk.
SWellFounded(((first(y))) c (x = pred(y)  E))
 (receives(dE; dL; pred?; info; p; e; l)
 ( ({r:E| rcv-from-on(dE; dL; info; e; l; r)}  List)) 

latex

Definitions	filter(P; l), eventlist(pred?; e), sends-bound(p; e; l), SWellFounded(R(x;y)), x,y. t(x;y), A c B, A, first(e), pred(e), x:A. B(x), rcv?(e), sender(e), link(e), P  Q, P  Q, e < e', loc(e), destination(l), Id, Unit, IdLnk, EqDecider(T), x. t(x), P  Q, receives(dE; dL; pred?; info; p; e; l), prop{i:l}, b, rcv-from-on(dE; dL; info; e; l; r), t  T, x:A. B(x), l_all(L; T; x.P(x))
Lemmas	rcv-from-on wf, assert wf, list set type, deq wf, IdLnk wf, unit wf, Id wf, ldst wf, loc wf, cless wf, link wf, sender wf, rcv? wf, pred wf, first wf, not wf, strongwellfounded wf, sends-bound wf, eventlist wf, filter wf, l all filter